A,B:Type. finite-type(A)  finite-type(B)  finite-type((A + B)) 

latex

Definitions	t  T, x:A. B(x), prop{i:l}, (x  l), P  Q, x:A. B(x), P  Q, P  Q, P  Q, finite-type(T), map(f; as), append(as; bs), guard(T), P  Q
Lemmas	finite-type wf, finite-type-iff-list, append wf, member append, or functionality wrt iff, member map, map wf, l member wf